Nuprl Lemma : p-filter_wf
11,40
postcript
pdf
T
:Type,
P
:(
T
),
f
:(
x
:
T
. Dec(
P
(
x
))). p-filter(
f
)
T
(
T
+ Top)
latex
ProofTree
Definitions
Type
,
t
T
,
,
x
:
A
B
(
x
)
,
f
(
a
)
,
x
(
s
)
,
x
:
A
.
B
(
x
)
,
A
,
left
+
right
,
P
Q
,
Void
,
x
:
A
.
B
(
x
)
,
Top
,
inr
x
,
inl
x
,
case
b
of inl(
x
) =>
s
(
x
) | inr(
y
) =>
t
(
y
)
,
x
.
A
(
x
)
,
p-filter(
f
)
,
Dec(
P
)
Lemmas
top
wf
,
not
wf
origin
T:Type, P:(T
), f:(x:T. Dec(P(x))). p-filter(f) 
T(T + Top)
T:Type, P:(T), f:(x:T. Dec(P(x))). p-filter(f) T(T + Top)
TB(x)x:A. B(x)
A
Q
x:A.B(x)
x.A(x)